YES 0.846 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule List
  ((genericLength :: [a ->  Int) :: [a ->  Int)

module List where
  import qualified Maybe
import qualified Prelude

  genericLength :: Num b => [a ->  b
genericLength [] 0
genericLength (_ : l+ genericLength l


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule List
  ((genericLength :: [a ->  Int) :: [a ->  Int)

module List where
  import qualified Maybe
import qualified Prelude

  genericLength :: Num b => [a ->  b
genericLength [] 0
genericLength (vw : l+ genericLength l


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ NumRed

mainModule List
  ((genericLength :: [a ->  Int) :: [a ->  Int)

module List where
  import qualified Maybe
import qualified Prelude

  genericLength :: Num b => [a ->  b
genericLength [] 0
genericLength (vw : l+ genericLength l


module Maybe where
  import qualified List
import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ NumRed
HASKELL
              ↳ Narrow

mainModule List
  (genericLength :: [a ->  Int)

module List where
  import qualified Maybe
import qualified Prelude

  genericLength :: Num a => [b ->  a
genericLength [] fromInt (Pos Zero)
genericLength (vw : lfromInt (Pos (Succ Zero)) + genericLength l


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ NumRed
            ↳ HASKELL
              ↳ Narrow
QDP
                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_genericLength(:(vz30, vz31), ba) → new_genericLength(vz31, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: